/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package expression;

import core.Node;
import core.UnsatException;
import domain.Domain;
import expression.interval.Interval;

/**
 *
 * @author ddoose
 */
public class Sum extends IntExpr {
    private int value;
    
    public Sum(Node n) {
        super(n);
        value = 0;
        current = Domain.UNIVERSE;
        target = Domain.UNIVERSE;
    }
    
    public Sum(Node n, int v) {
        super(n);
        value = v;
        current = Domain.UNIVERSE;
        target = Domain.UNIVERSE;
    }
    
    public Sum(Node c, IntExpr[] p) {
        super(c, p);
        value = 0;
        current = Domain.UNIVERSE;
        target = Domain.UNIVERSE;
    }

    public Sum(Node c, IntExpr[] p, int v) {
        super(c, p);
        value = v;
        current = Domain.UNIVERSE;
        target = Domain.UNIVERSE;
    }

    public boolean same(IntExpr i) {
        return (i instanceof Sum) && sameParameters(i) && (value == ((Sum)i).value);
    }

    public void eval() throws UnsatException {
        Domain newD = Domain.UNIVERSE;
        boolean lb = true;
        int l = 0;
        boolean rb = true;
        int r = 0;
        
        for (int i: getParameters()) {
            Domain p = node.getIntExpr(i).current;
            if (lb && (p.isLeftBounded())) {
                l += p.getLeftBound();
            }
            else {
                lb = false;
            }
            if (rb && (p.isRightBounded())) {
                r += p.getRightBound();
            }
            else {
                rb = false;
            }
            if (!lb && !rb)
                break;
        }
        if (lb && rb) {
            newD = new Domain(Interval.createBounded(l + value, r + value));
        }
        else if (lb) {
            newD = new Domain(Interval.createLeftBounded(l + value));
        }
        else if (rb) {
            newD = new Domain(Interval.createRightBounded(r + value));
        }
        else {
            newD = new Domain(Interval.createUniverse());
        }
        
        reduceCurrent(newD);
    }

    public void propagate() throws UnsatException {
        // LEFT
        if (target.isLeftBounded()) {
            for (int i: getParameters()) {
                IntExpr p = node.getIntExpr(i);
                boolean b = true;
                int v = 0;
                for (int j: getParameters()) {
                    IntExpr pp = node.getIntExpr(j);
                    if (i != j) {
                        if (pp.current.isRightBounded()) {
                            v += pp.current.getRightBound();
                        }
                        else {
                            b = false;
                            break;
                        }
                    }
                }
                if (b) {
                    Domain d = new Domain(Interval.createLeftBounded(target.getLeftBound() - v - value));
                    p.reduceTarget(d);
                }
            }
        }

        // RIGHT
        if (target.isRightBounded()) {
            for (int i: getParameters()) {
                IntExpr p = node.getIntExpr(i);
                boolean b = true;
                int v = 0;
                for (int j: getParameters()) {
                    IntExpr pp = node.getIntExpr(j);
                    if (p != pp) {
                        if (pp.current.isLeftBounded()) {
                            v += pp.current.getLeftBound();
                        }
                        else {
                            b = false;
                            break;
                        }
                    }
                }
                if (b) {
                    Domain d = new Domain(Interval.createRightBounded(target.getRightBound() - v - value));
                    p.reduceTarget(d);
                }
            }
        }
    }
    
    public boolean reduce() {
        // si valeur
        if (current.isValue()) {
            Value v = node.createValue(current.getValue());
            node.replaceIntExpr(id, v.getId());
            return true;
        }

        boolean b = false;
        // on regroupe toutes les valeurs
        for (int i = 0; i < getParameters().size(); i++) {
            IntExpr p = node.getIntExpr(getParameters().get(i));
            if (p.current.isValue()) {
                value += p.current.getValue();
                node.removeDependency(id, p.getId());
                i--;
                b = true;
            }
        }
        
        // si plus de paramètres
        if (getParameters().size() == 0) {
            Value v = node.createValue(value);
            node.replaceIntExpr(id, v.getId());
            return true;
        }      
        return b;
    }
    
    public Sum clone(Node n) {
        Sum sum = new Sum(n, value);
        sum.clone(this);
        return sum;
    }

    public String toString() {
        String s = "(+";
        
        for (int i: getParameters()) {
            IntExpr p = node.getIntExpr(i);
            s += " " + p;
        }
        
        s += " " + value + ")";
        
        return s;
    }
    
    public String pretty() {
        return id + "\t" + current + "\t" + target + "\t" + toString();
    }
}
